:: FLANG_2 semantic presentation

begin

theorem :: FLANG_2:1
for m, k, i, n being ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) st m : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) + k : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) : ( ( ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) set ) <= i : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) & i : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) <= n : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) + k : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) : ( ( ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) set ) holds
ex mn being ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) st
( mn : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) + k : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) : ( ( ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) set ) = i : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) & m : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) <= mn : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) & mn : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) <= n : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) ) ;

theorem :: FLANG_2:2
for m, n, k, l, i being ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) st m : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) <= n : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) & k : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) <= l : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) & m : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) + k : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) : ( ( ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) set ) <= i : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) & i : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) <= n : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) + l : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) : ( ( ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) set ) holds
ex mn, kl being ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) st
( mn : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) + kl : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) : ( ( ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) set ) = i : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) & m : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) <= mn : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) & mn : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) <= n : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) & k : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) <= kl : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) & kl : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) <= l : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) ) ;

theorem :: FLANG_2:3
for m, n being ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) st m : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) < n : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) holds
ex k being ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) st
( m : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) + k : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) : ( ( ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) set ) = n : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) & k : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) > 0 : ( ( ) ( empty V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative V15() V16() V17() V18( NAT : ( ( ) ( non empty V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) V20() V21() V22() V23() V32() V33() V34() V37() V51() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) ;

theorem :: FLANG_2:4
for E being ( ( ) ( ) set )
for a, b being ( ( ) ( V8() V15() V18( NAT : ( ( ) ( non empty V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) V20() V33() V51() ) Element of E : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty V23() ) set ) ) st ( a : ( ( ) ( V8() V15() V18( NAT : ( ( ) ( non empty V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) V20() V33() V51() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty V23() ) set ) ) ^ b : ( ( ) ( V8() V15() V18( NAT : ( ( ) ( non empty V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) V20() V33() V51() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty V23() ) set ) ) : ( ( ) ( V8() V15() V18( NAT : ( ( ) ( non empty V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) V20() V33() V51() ) Element of K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) = a : ( ( ) ( V8() V15() V18( NAT : ( ( ) ( non empty V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) V20() V33() V51() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty V23() ) set ) ) or b : ( ( ) ( V8() V15() V18( NAT : ( ( ) ( non empty V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) V20() V33() V51() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty V23() ) set ) ) ^ a : ( ( ) ( V8() V15() V18( NAT : ( ( ) ( non empty V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) V20() V33() V51() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty V23() ) set ) ) : ( ( ) ( V8() V15() V18( NAT : ( ( ) ( non empty V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) V20() V33() V51() ) Element of K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) = a : ( ( ) ( V8() V15() V18( NAT : ( ( ) ( non empty V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) V20() V33() V51() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty V23() ) set ) ) ) holds
b : ( ( ) ( V8() V15() V18( NAT : ( ( ) ( non empty V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) V20() V33() V51() ) Element of b1 : ( ( ) ( ) set ) ^omega : ( ( ) ( non empty V23() ) set ) ) = {} : ( ( ) ( empty V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative V15() V16() V17() V18( NAT : ( ( ) ( non empty V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) V20() V21() V22() V23() V32() V33() V34() V37() V51() ) set ) ;

begin

theorem :: FLANG_2:5
for x, E being ( ( ) ( ) set )
for A, B being ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) st ( x : ( ( ) ( ) set ) in A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) or x : ( ( ) ( ) set ) in B : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) ) & x : ( ( ) ( ) set ) <> <%> E : ( ( ) ( ) set ) : ( ( ) ( empty V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative V15() V16() V17() V18( NAT : ( ( ) ( non empty V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) V19(b2 : ( ( ) ( ) set ) ) V20() V21() V22() V23() V32() V33() V34() V37() V51() ) Element of K231(b2 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b2 : ( ( ) ( ) set ) )) ) holds
A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) ^^ B : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( V23() ) Element of K6(K231(b2 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b2 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) <> {(<%> E : ( ( ) ( ) set ) ) : ( ( ) ( empty V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative V15() V16() V17() V18( NAT : ( ( ) ( non empty V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) V19(b2 : ( ( ) ( ) set ) ) V20() V21() V22() V23() V32() V33() V34() V37() V51() ) Element of K231(b2 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b2 : ( ( ) ( ) set ) )) ) } : ( ( ) ( non empty V23() V33() V37() ) Element of K6(K231(b2 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b2 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) ;

theorem :: FLANG_2:6
for x, E being ( ( ) ( ) set )
for A, B being ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) holds
( <%x : ( ( ) ( ) set ) %> : ( ( V15() V20() ) ( non empty V8() V15() V18( NAT : ( ( ) ( non empty V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) V20() V33() V40(1 : ( ( ) ( non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V51() ) set ) in A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) ^^ B : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( V23() ) Element of K6(K231(b2 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b2 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) iff ( ( <%> E : ( ( ) ( ) set ) : ( ( ) ( empty V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative V15() V16() V17() V18( NAT : ( ( ) ( non empty V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) V19(b2 : ( ( ) ( ) set ) ) V20() V21() V22() V23() V32() V33() V34() V37() V51() ) Element of K231(b2 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b2 : ( ( ) ( ) set ) )) ) in A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) & <%x : ( ( ) ( ) set ) %> : ( ( V15() V20() ) ( non empty V8() V15() V18( NAT : ( ( ) ( non empty V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) V20() V33() V40(1 : ( ( ) ( non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V51() ) set ) in B : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) ) or ( <%x : ( ( ) ( ) set ) %> : ( ( V15() V20() ) ( non empty V8() V15() V18( NAT : ( ( ) ( non empty V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) V20() V33() V40(1 : ( ( ) ( non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V51() ) set ) in A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) & <%> E : ( ( ) ( ) set ) : ( ( ) ( empty V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative V15() V16() V17() V18( NAT : ( ( ) ( non empty V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) V19(b2 : ( ( ) ( ) set ) ) V20() V21() V22() V23() V32() V33() V34() V37() V51() ) Element of K231(b2 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b2 : ( ( ) ( ) set ) )) ) in B : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) ) ) ) ;

theorem :: FLANG_2:7
for x, E being ( ( ) ( ) set )
for A being ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) )
for n being ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) st x : ( ( ) ( ) set ) in A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) & x : ( ( ) ( ) set ) <> <%> E : ( ( ) ( ) set ) : ( ( ) ( empty V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative V15() V16() V17() V18( NAT : ( ( ) ( non empty V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) V19(b2 : ( ( ) ( ) set ) ) V20() V21() V22() V23() V32() V33() V34() V37() V51() ) Element of K231(b2 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b2 : ( ( ) ( ) set ) )) ) & n : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) > 0 : ( ( ) ( empty V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative V15() V16() V17() V18( NAT : ( ( ) ( non empty V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) V20() V21() V22() V23() V32() V33() V34() V37() V51() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) holds
A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) |^ n : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) : ( ( ) ( V23() ) Element of K6(K231(b2 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b2 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) <> {(<%> E : ( ( ) ( ) set ) ) : ( ( ) ( empty V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative V15() V16() V17() V18( NAT : ( ( ) ( non empty V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) V19(b2 : ( ( ) ( ) set ) ) V20() V21() V22() V23() V32() V33() V34() V37() V51() ) Element of K231(b2 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b2 : ( ( ) ( ) set ) )) ) } : ( ( ) ( non empty V23() V33() V37() ) Element of K6(K231(b2 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b2 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) ;

theorem :: FLANG_2:8
for E being ( ( ) ( ) set )
for A being ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) )
for n being ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) holds
( <%> E : ( ( ) ( ) set ) : ( ( ) ( empty V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative V15() V16() V17() V18( NAT : ( ( ) ( non empty V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) V19(b1 : ( ( ) ( ) set ) ) V20() V21() V22() V23() V32() V33() V34() V37() V51() ) Element of K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) in A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) |^ n : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) : ( ( ) ( V23() ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) iff ( n : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) = 0 : ( ( ) ( empty V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative V15() V16() V17() V18( NAT : ( ( ) ( non empty V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) V20() V21() V22() V23() V32() V33() V34() V37() V51() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) or <%> E : ( ( ) ( ) set ) : ( ( ) ( empty V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative V15() V16() V17() V18( NAT : ( ( ) ( non empty V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) V19(b1 : ( ( ) ( ) set ) ) V20() V21() V22() V23() V32() V33() V34() V37() V51() ) Element of K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) in A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) ) ) ;

theorem :: FLANG_2:9
for x, E being ( ( ) ( ) set )
for A being ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) )
for n being ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) holds
( <%x : ( ( ) ( ) set ) %> : ( ( V15() V20() ) ( non empty V8() V15() V18( NAT : ( ( ) ( non empty V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) V20() V33() V40(1 : ( ( ) ( non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V51() ) set ) in A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) |^ n : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) : ( ( ) ( V23() ) Element of K6(K231(b2 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b2 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) iff ( <%x : ( ( ) ( ) set ) %> : ( ( V15() V20() ) ( non empty V8() V15() V18( NAT : ( ( ) ( non empty V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) V20() V33() V40(1 : ( ( ) ( non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V51() ) set ) in A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) & ( ( <%> E : ( ( ) ( ) set ) : ( ( ) ( empty V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative V15() V16() V17() V18( NAT : ( ( ) ( non empty V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) V19(b2 : ( ( ) ( ) set ) ) V20() V21() V22() V23() V32() V33() V34() V37() V51() ) Element of K231(b2 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b2 : ( ( ) ( ) set ) )) ) in A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) & n : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) > 1 : ( ( ) ( non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) or n : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) = 1 : ( ( ) ( non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) ) ) ;

theorem :: FLANG_2:10
for x, E being ( ( ) ( ) set )
for A being ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) )
for m, n being ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) st m : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) <> n : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) & A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) |^ m : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) : ( ( ) ( V23() ) Element of K6(K231(b2 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b2 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) = {x : ( ( ) ( ) set ) } : ( ( ) ( non empty V33() ) set ) & A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) |^ n : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) : ( ( ) ( V23() ) Element of K6(K231(b2 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b2 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) = {x : ( ( ) ( ) set ) } : ( ( ) ( non empty V33() ) set ) holds
x : ( ( ) ( ) set ) = <%> E : ( ( ) ( ) set ) : ( ( ) ( empty V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative V15() V16() V17() V18( NAT : ( ( ) ( non empty V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) V19(b2 : ( ( ) ( ) set ) ) V20() V21() V22() V23() V32() V33() V34() V37() V51() ) Element of K231(b2 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b2 : ( ( ) ( ) set ) )) ) ;

theorem :: FLANG_2:11
for E being ( ( ) ( ) set )
for A being ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) )
for m, n being ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) holds (A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) |^ m : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) ) : ( ( ) ( V23() ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) |^ n : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) : ( ( ) ( V23() ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) = (A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) |^ n : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) ) : ( ( ) ( V23() ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) |^ m : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) : ( ( ) ( V23() ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) ;

theorem :: FLANG_2:12
for E being ( ( ) ( ) set )
for A being ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) )
for m, n being ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) holds (A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) |^ m : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) ) : ( ( ) ( V23() ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) ^^ (A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) |^ n : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) ) : ( ( ) ( V23() ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( V23() ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) = (A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) |^ n : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) ) : ( ( ) ( V23() ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) ^^ (A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) |^ m : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) ) : ( ( ) ( V23() ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( V23() ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) ;

theorem :: FLANG_2:13
for E being ( ( ) ( ) set )
for B, A being ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) )
for l being ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) st <%> E : ( ( ) ( ) set ) : ( ( ) ( empty V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative V15() V16() V17() V18( NAT : ( ( ) ( non empty V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) V19(b1 : ( ( ) ( ) set ) ) V20() V21() V22() V23() V32() V33() V34() V37() V51() ) Element of K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) in B : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) holds
( A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) c= A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) ^^ (B : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) |^ l : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) ) : ( ( ) ( V23() ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( V23() ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) & A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) c= (B : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) |^ l : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) ) : ( ( ) ( V23() ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) ^^ A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( V23() ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) ) ;

theorem :: FLANG_2:14
for E being ( ( ) ( ) set )
for A, C, B being ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) )
for k, l being ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) st A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) c= C : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) |^ k : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) : ( ( ) ( V23() ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) & B : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) c= C : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) |^ l : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) : ( ( ) ( V23() ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) holds
A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) ^^ B : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( V23() ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) c= C : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) |^ (k : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) + l : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) ) : ( ( ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) set ) : ( ( ) ( V23() ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) ;

theorem :: FLANG_2:15
for x, E being ( ( ) ( ) set )
for A being ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) st x : ( ( ) ( ) set ) in A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) & x : ( ( ) ( ) set ) <> <%> E : ( ( ) ( ) set ) : ( ( ) ( empty V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative V15() V16() V17() V18( NAT : ( ( ) ( non empty V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) V19(b2 : ( ( ) ( ) set ) ) V20() V21() V22() V23() V32() V33() V34() V37() V51() ) Element of K231(b2 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b2 : ( ( ) ( ) set ) )) ) holds
A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) * : ( ( ) ( V23() ) Element of K6(K231(b2 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b2 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) <> {(<%> E : ( ( ) ( ) set ) ) : ( ( ) ( empty V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative V15() V16() V17() V18( NAT : ( ( ) ( non empty V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) V19(b2 : ( ( ) ( ) set ) ) V20() V21() V22() V23() V32() V33() V34() V37() V51() ) Element of K231(b2 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b2 : ( ( ) ( ) set ) )) ) } : ( ( ) ( non empty V23() V33() V37() ) Element of K6(K231(b2 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b2 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) ;

theorem :: FLANG_2:16
for E being ( ( ) ( ) set )
for A being ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) )
for n being ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) st <%> E : ( ( ) ( ) set ) : ( ( ) ( empty V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative V15() V16() V17() V18( NAT : ( ( ) ( non empty V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) V19(b1 : ( ( ) ( ) set ) ) V20() V21() V22() V23() V32() V33() V34() V37() V51() ) Element of K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) in A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) & n : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) > 0 : ( ( ) ( empty V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative V15() V16() V17() V18( NAT : ( ( ) ( non empty V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) V20() V21() V22() V23() V32() V33() V34() V37() V51() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) holds
(A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) |^ n : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) ) : ( ( ) ( V23() ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) * : ( ( ) ( V23() ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) = A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) * : ( ( ) ( V23() ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) ;

theorem :: FLANG_2:17
for E being ( ( ) ( ) set )
for A being ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) )
for n being ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) st <%> E : ( ( ) ( ) set ) : ( ( ) ( empty V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative V15() V16() V17() V18( NAT : ( ( ) ( non empty V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) V19(b1 : ( ( ) ( ) set ) ) V20() V21() V22() V23() V32() V33() V34() V37() V51() ) Element of K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) in A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) holds
(A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) |^ n : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) ) : ( ( ) ( V23() ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) * : ( ( ) ( V23() ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) = (A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) *) : ( ( ) ( V23() ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) |^ n : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) : ( ( ) ( V23() ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) ;

theorem :: FLANG_2:18
for E being ( ( ) ( ) set )
for A, B being ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) holds
( A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) c= A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) ^^ (B : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) *) : ( ( ) ( V23() ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( V23() ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) & A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) c= (B : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) *) : ( ( ) ( V23() ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) ^^ A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( V23() ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) ) ;

begin

definition
let E be ( ( ) ( ) set ) ;
let A be ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) ;
let m, n be ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) ;
func A |^ (m,n) -> ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) equals :: FLANG_2:def 1
 union { B : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) where B is ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) : ex k being ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) st
( m : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) set ) <= k : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) & k : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) <= n : ( ( ) ( ) set ) & B : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) = A : ( ( ) ( V23() ) Element of K6(K231(E : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(E : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) |^ k : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) : ( ( ) ( V23() ) Element of K6(K231(E : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(E : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) ) } : ( ( ) ( ) set ) ;
end;

theorem :: FLANG_2:19
for E, x being ( ( ) ( ) set )
for A being ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) )
for m, n being ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) holds
( x : ( ( ) ( ) set ) in A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) |^ (m : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) ,n : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) ) : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) iff ex k being ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) st
( m : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) <= k : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) & k : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) <= n : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) & x : ( ( ) ( ) set ) in A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) |^ k : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) : ( ( ) ( V23() ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) ) ) ;

theorem :: FLANG_2:20
for E being ( ( ) ( ) set )
for A being ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) )
for m, k, n being ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) st m : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) <= k : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) & k : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) <= n : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) holds
A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) |^ k : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) : ( ( ) ( V23() ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) c= A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) |^ (m : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) ,n : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) ) : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) ;

theorem :: FLANG_2:21
for E being ( ( ) ( ) set )
for A being ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) )
for m, n being ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) holds
( A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) |^ (m : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) ,n : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) ) : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) = {} : ( ( ) ( empty V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative V15() V16() V17() V18( NAT : ( ( ) ( non empty V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) V20() V21() V22() V23() V32() V33() V34() V37() V51() ) set ) iff ( m : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) > n : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) or ( m : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) > 0 : ( ( ) ( empty V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative V15() V16() V17() V18( NAT : ( ( ) ( non empty V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) V20() V21() V22() V23() V32() V33() V34() V37() V51() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) & A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) = {} : ( ( ) ( empty V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative V15() V16() V17() V18( NAT : ( ( ) ( non empty V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) V20() V21() V22() V23() V32() V33() V34() V37() V51() ) set ) ) ) ) ;

theorem :: FLANG_2:22
for E being ( ( ) ( ) set )
for A being ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) )
for m being ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) holds A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) |^ (m : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) ,m : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) ) : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) = A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) |^ m : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) : ( ( ) ( V23() ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) ;

theorem :: FLANG_2:23
for E being ( ( ) ( ) set )
for A being ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) )
for m, k, l, n being ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) st m : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) <= k : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) & l : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) <= n : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) holds
A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) |^ (k : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) ,l : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) ) : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) c= A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) |^ (m : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) ,n : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) ) : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) ;

theorem :: FLANG_2:24
for E being ( ( ) ( ) set )
for A being ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) )
for m, k, n being ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) st m : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) <= k : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) & k : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) <= n : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) holds
A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) |^ (m : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) ,n : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) ) : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) = (A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) |^ (m : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) ,k : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) )) : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) \/ (A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) |^ (k : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) ,n : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) )) : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( V23() ) Element of K6((b1 : ( ( ) ( ) set ) ^omega) : ( ( ) ( non empty V23() ) set ) ) : ( ( ) ( non empty ) set ) ) ;

theorem :: FLANG_2:25
for E being ( ( ) ( ) set )
for A being ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) )
for m, k, n being ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) st m : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) <= k : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) & k : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) <= n : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) holds
A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) |^ (m : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) ,n : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) ) : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) = (A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) |^ (m : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) ,k : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) )) : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) \/ (A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) |^ ((k : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) + 1 : ( ( ) ( non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() ) set ) ,n : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) )) : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( V23() ) Element of K6((b1 : ( ( ) ( ) set ) ^omega) : ( ( ) ( non empty V23() ) set ) ) : ( ( ) ( non empty ) set ) ) ;

theorem :: FLANG_2:26
for E being ( ( ) ( ) set )
for A being ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) )
for m, n being ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) st m : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) <= n : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) + 1 : ( ( ) ( non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() ) set ) holds
A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) |^ (m : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) ,(n : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) + 1 : ( ( ) ( non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() ) set ) ) : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) = (A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) |^ (m : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) ,n : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) )) : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) \/ (A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) |^ (n : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) + 1 : ( ( ) ( non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() ) set ) ) : ( ( ) ( V23() ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( V23() ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) ;

theorem :: FLANG_2:27
for E being ( ( ) ( ) set )
for A being ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) )
for m, n being ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) st m : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) <= n : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) holds
A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) |^ (m : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) ,n : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) ) : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) = (A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) |^ m : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) ) : ( ( ) ( V23() ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) \/ (A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) |^ ((m : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) + 1 : ( ( ) ( non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() ) set ) ,n : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) )) : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( V23() ) Element of K6((b1 : ( ( ) ( ) set ) ^omega) : ( ( ) ( non empty V23() ) set ) ) : ( ( ) ( non empty ) set ) ) ;

theorem :: FLANG_2:28
for E being ( ( ) ( ) set )
for A being ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) )
for n being ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) holds A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) |^ (n : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) ,(n : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) + 1 : ( ( ) ( non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() ) set ) ) : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) = (A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) |^ n : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) ) : ( ( ) ( V23() ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) \/ (A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) |^ (n : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) + 1 : ( ( ) ( non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() ) set ) ) : ( ( ) ( V23() ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( V23() ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) ;

theorem :: FLANG_2:29
for E being ( ( ) ( ) set )
for A, B being ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) )
for m, n being ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) st A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) c= B : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) holds
A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) |^ (m : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) ,n : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) ) : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) c= B : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) |^ (m : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) ,n : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) ) : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) ;

theorem :: FLANG_2:30
for x, E being ( ( ) ( ) set )
for A being ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) )
for m, n being ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) st x : ( ( ) ( ) set ) in A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) & x : ( ( ) ( ) set ) <> <%> E : ( ( ) ( ) set ) : ( ( ) ( empty V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative V15() V16() V17() V18( NAT : ( ( ) ( non empty V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) V19(b2 : ( ( ) ( ) set ) ) V20() V21() V22() V23() V32() V33() V34() V37() V51() ) Element of K231(b2 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b2 : ( ( ) ( ) set ) )) ) & ( m : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) > 0 : ( ( ) ( empty V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative V15() V16() V17() V18( NAT : ( ( ) ( non empty V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) V20() V21() V22() V23() V32() V33() V34() V37() V51() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) or n : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) > 0 : ( ( ) ( empty V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative V15() V16() V17() V18( NAT : ( ( ) ( non empty V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) V20() V21() V22() V23() V32() V33() V34() V37() V51() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) holds
A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) |^ (m : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) ,n : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) ) : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) <> {(<%> E : ( ( ) ( ) set ) ) : ( ( ) ( empty V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative V15() V16() V17() V18( NAT : ( ( ) ( non empty V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) V19(b2 : ( ( ) ( ) set ) ) V20() V21() V22() V23() V32() V33() V34() V37() V51() ) Element of K231(b2 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b2 : ( ( ) ( ) set ) )) ) } : ( ( ) ( non empty V23() V33() V37() ) Element of K6(K231(b2 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b2 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) ;

theorem :: FLANG_2:31
for E being ( ( ) ( ) set )
for A being ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) )
for m, n being ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) holds
( A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) |^ (m : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) ,n : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) ) : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) = {(<%> E : ( ( ) ( ) set ) ) : ( ( ) ( empty V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative V15() V16() V17() V18( NAT : ( ( ) ( non empty V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) V19(b1 : ( ( ) ( ) set ) ) V20() V21() V22() V23() V32() V33() V34() V37() V51() ) Element of K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) } : ( ( ) ( non empty V23() V33() V37() ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) iff ( ( m : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) <= n : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) & A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) = {(<%> E : ( ( ) ( ) set ) ) : ( ( ) ( empty V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative V15() V16() V17() V18( NAT : ( ( ) ( non empty V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) V19(b1 : ( ( ) ( ) set ) ) V20() V21() V22() V23() V32() V33() V34() V37() V51() ) Element of K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) } : ( ( ) ( non empty V23() V33() V37() ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) ) or ( m : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) = 0 : ( ( ) ( empty V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative V15() V16() V17() V18( NAT : ( ( ) ( non empty V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) V20() V21() V22() V23() V32() V33() V34() V37() V51() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) & n : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) = 0 : ( ( ) ( empty V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative V15() V16() V17() V18( NAT : ( ( ) ( non empty V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) V20() V21() V22() V23() V32() V33() V34() V37() V51() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) or ( m : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) = 0 : ( ( ) ( empty V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative V15() V16() V17() V18( NAT : ( ( ) ( non empty V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) V20() V21() V22() V23() V32() V33() V34() V37() V51() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) & A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) = {} : ( ( ) ( empty V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative V15() V16() V17() V18( NAT : ( ( ) ( non empty V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) V20() V21() V22() V23() V32() V33() V34() V37() V51() ) set ) ) ) ) ;

theorem :: FLANG_2:32
for E being ( ( ) ( ) set )
for A being ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) )
for m, n being ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) holds A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) |^ (m : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) ,n : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) ) : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) c= A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) * : ( ( ) ( V23() ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) ;

theorem :: FLANG_2:33
for E being ( ( ) ( ) set )
for A being ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) )
for m, n being ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) holds
( <%> E : ( ( ) ( ) set ) : ( ( ) ( empty V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative V15() V16() V17() V18( NAT : ( ( ) ( non empty V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) V19(b1 : ( ( ) ( ) set ) ) V20() V21() V22() V23() V32() V33() V34() V37() V51() ) Element of K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) in A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) |^ (m : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) ,n : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) ) : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) iff ( m : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) = 0 : ( ( ) ( empty V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative V15() V16() V17() V18( NAT : ( ( ) ( non empty V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) V20() V21() V22() V23() V32() V33() V34() V37() V51() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) or ( m : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) <= n : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) & <%> E : ( ( ) ( ) set ) : ( ( ) ( empty V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative V15() V16() V17() V18( NAT : ( ( ) ( non empty V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) V19(b1 : ( ( ) ( ) set ) ) V20() V21() V22() V23() V32() V33() V34() V37() V51() ) Element of K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) in A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) ) ) ) ;

theorem :: FLANG_2:34
for E being ( ( ) ( ) set )
for A being ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) )
for m, n being ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) st <%> E : ( ( ) ( ) set ) : ( ( ) ( empty V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative V15() V16() V17() V18( NAT : ( ( ) ( non empty V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) V19(b1 : ( ( ) ( ) set ) ) V20() V21() V22() V23() V32() V33() V34() V37() V51() ) Element of K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) in A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) & m : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) <= n : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) holds
A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) |^ (m : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) ,n : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) ) : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) = A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) |^ n : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) : ( ( ) ( V23() ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) ;

theorem :: FLANG_2:35
for E being ( ( ) ( ) set )
for A being ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) )
for m, n, k being ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) holds (A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) |^ (m : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) ,n : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) )) : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) ^^ (A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) |^ k : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) ) : ( ( ) ( V23() ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( V23() ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) = (A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) |^ k : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) ) : ( ( ) ( V23() ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) ^^ (A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) |^ (m : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) ,n : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) )) : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( V23() ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) ;

theorem :: FLANG_2:36
for E being ( ( ) ( ) set )
for A being ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) )
for m, n being ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) holds (A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) |^ (m : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) ,n : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) )) : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) ^^ A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( V23() ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) = A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) ^^ (A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) |^ (m : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) ,n : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) )) : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( V23() ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) ;

theorem :: FLANG_2:37
for E being ( ( ) ( ) set )
for A being ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) )
for m, n, k, l being ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) st m : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) <= n : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) & k : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) <= l : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) holds
(A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) |^ (m : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) ,n : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) )) : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) ^^ (A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) |^ (k : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) ,l : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) )) : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( V23() ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) = A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) |^ ((m : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) + k : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) ) : ( ( ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) set ) ,(n : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) + l : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) ) : ( ( ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) set ) ) : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) ;

theorem :: FLANG_2:38
for E being ( ( ) ( ) set )
for A being ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) )
for m, n being ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) holds A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) |^ ((m : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) + 1 : ( ( ) ( non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() ) set ) ,(n : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) + 1 : ( ( ) ( non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() ) set ) ) : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) = (A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) |^ (m : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) ,n : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) )) : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) ^^ A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( V23() ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) ;

theorem :: FLANG_2:39
for E being ( ( ) ( ) set )
for A being ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) )
for m, n, k, l being ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) holds (A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) |^ (m : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) ,n : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) )) : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) ^^ (A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) |^ (k : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) ,l : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) )) : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( V23() ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) = (A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) |^ (k : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) ,l : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) )) : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) ^^ (A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) |^ (m : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) ,n : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) )) : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( V23() ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) ;

theorem :: FLANG_2:40
for E being ( ( ) ( ) set )
for A being ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) )
for m, n, k being ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) holds (A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) |^ (m : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) ,n : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) )) : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) |^ k : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) : ( ( ) ( V23() ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) = A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) |^ ((m : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) * k : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) ) : ( ( ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) set ) ,(n : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) * k : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) ) : ( ( ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) set ) ) : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) ;

theorem :: FLANG_2:41
for E being ( ( ) ( ) set )
for A being ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) )
for k, m, n being ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) holds (A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) |^ (k : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) + 1 : ( ( ) ( non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() ) set ) ) : ( ( ) ( V23() ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) |^ (m : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) ,n : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) ) : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) c= ((A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) |^ k : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) ) : ( ( ) ( V23() ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) |^ (m : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) ,n : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) )) : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) ^^ (A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) |^ (m : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) ,n : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) )) : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( V23() ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) ;

theorem :: FLANG_2:42
for E being ( ( ) ( ) set )
for A being ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) )
for k, m, n being ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) holds (A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) |^ k : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) ) : ( ( ) ( V23() ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) |^ (m : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) ,n : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) ) : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) c= A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) |^ ((k : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) * m : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) ) : ( ( ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) set ) ,(k : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) * n : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) ) : ( ( ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) set ) ) : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) ;

theorem :: FLANG_2:43
for E being ( ( ) ( ) set )
for A being ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) )
for k, m, n being ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) holds (A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) |^ k : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) ) : ( ( ) ( V23() ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) |^ (m : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) ,n : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) ) : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) c= (A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) |^ (m : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) ,n : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) )) : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) |^ k : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) : ( ( ) ( V23() ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) ;

theorem :: FLANG_2:44
for E being ( ( ) ( ) set )
for A being ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) )
for k, l, m, n being ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) holds (A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) |^ (k : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) + l : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) ) : ( ( ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) set ) ) : ( ( ) ( V23() ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) |^ (m : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) ,n : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) ) : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) c= ((A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) |^ k : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) ) : ( ( ) ( V23() ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) |^ (m : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) ,n : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) )) : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) ^^ ((A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) |^ l : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) ) : ( ( ) ( V23() ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) |^ (m : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) ,n : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) )) : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( V23() ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) ;

theorem :: FLANG_2:45
for E being ( ( ) ( ) set )
for A being ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) holds A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) |^ (0 : ( ( ) ( empty V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative V15() V16() V17() V18( NAT : ( ( ) ( non empty V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) V20() V21() V22() V23() V32() V33() V34() V37() V51() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) ,0 : ( ( ) ( empty V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative V15() V16() V17() V18( NAT : ( ( ) ( non empty V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) V20() V21() V22() V23() V32() V33() V34() V37() V51() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) = {(<%> E : ( ( ) ( ) set ) ) : ( ( ) ( empty V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative V15() V16() V17() V18( NAT : ( ( ) ( non empty V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) V19(b1 : ( ( ) ( ) set ) ) V20() V21() V22() V23() V32() V33() V34() V37() V51() ) Element of K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) } : ( ( ) ( non empty V23() V33() V37() ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) ;

theorem :: FLANG_2:46
for E being ( ( ) ( ) set )
for A being ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) holds A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) |^ (0 : ( ( ) ( empty V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative V15() V16() V17() V18( NAT : ( ( ) ( non empty V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) V20() V21() V22() V23() V32() V33() V34() V37() V51() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) = {(<%> E : ( ( ) ( ) set ) ) : ( ( ) ( empty V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative V15() V16() V17() V18( NAT : ( ( ) ( non empty V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) V19(b1 : ( ( ) ( ) set ) ) V20() V21() V22() V23() V32() V33() V34() V37() V51() ) Element of K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) } : ( ( ) ( non empty V23() V33() V37() ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) \/ A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty V23() ) Element of K6((b1 : ( ( ) ( ) set ) ^omega) : ( ( ) ( non empty V23() ) set ) ) : ( ( ) ( non empty ) set ) ) ;

theorem :: FLANG_2:47
for E being ( ( ) ( ) set )
for A being ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) holds A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) |^ (1 : ( ( ) ( non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) = A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) ;

theorem :: FLANG_2:48
for E being ( ( ) ( ) set )
for A being ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) holds A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) |^ (0 : ( ( ) ( empty V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative V15() V16() V17() V18( NAT : ( ( ) ( non empty V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) V20() V21() V22() V23() V32() V33() V34() V37() V51() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) ,2 : ( ( ) ( non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) = ({(<%> E : ( ( ) ( ) set ) ) : ( ( ) ( empty V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative V15() V16() V17() V18( NAT : ( ( ) ( non empty V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) V19(b1 : ( ( ) ( ) set ) ) V20() V21() V22() V23() V32() V33() V34() V37() V51() ) Element of K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) } : ( ( ) ( non empty V23() V33() V37() ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) \/ A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty V23() ) Element of K6((b1 : ( ( ) ( ) set ) ^omega) : ( ( ) ( non empty V23() ) set ) ) : ( ( ) ( non empty ) set ) ) \/ (A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) ^^ A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( V23() ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty V23() ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) ;

theorem :: FLANG_2:49
for E being ( ( ) ( ) set )
for A being ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) holds A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) |^ (1 : ( ( ) ( non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) ,2 : ( ( ) ( non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) = A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) \/ (A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) ^^ A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( V23() ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( V23() ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) ;

theorem :: FLANG_2:50
for E being ( ( ) ( ) set )
for A being ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) holds A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) |^ (2 : ( ( ) ( non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) ,2 : ( ( ) ( non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) = A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) ^^ A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( V23() ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) ;

theorem :: FLANG_2:51
for E, x being ( ( ) ( ) set )
for A being ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) )
for m, n being ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) st m : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) > 0 : ( ( ) ( empty V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative V15() V16() V17() V18( NAT : ( ( ) ( non empty V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) V20() V21() V22() V23() V32() V33() V34() V37() V51() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) & A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) |^ (m : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) ,n : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) ) : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) = {x : ( ( ) ( ) set ) } : ( ( ) ( non empty V33() ) set ) holds
for mn being ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) st m : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) <= mn : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) & mn : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) <= n : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) holds
A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) |^ mn : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) : ( ( ) ( V23() ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) = {x : ( ( ) ( ) set ) } : ( ( ) ( non empty V33() ) set ) ;

theorem :: FLANG_2:52
for x, E being ( ( ) ( ) set )
for A being ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) )
for m, n being ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) st m : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) <> n : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) & A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) |^ (m : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) ,n : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) ) : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) = {x : ( ( ) ( ) set ) } : ( ( ) ( non empty V33() ) set ) holds
x : ( ( ) ( ) set ) = <%> E : ( ( ) ( ) set ) : ( ( ) ( empty V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative V15() V16() V17() V18( NAT : ( ( ) ( non empty V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) V19(b2 : ( ( ) ( ) set ) ) V20() V21() V22() V23() V32() V33() V34() V37() V51() ) Element of K231(b2 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b2 : ( ( ) ( ) set ) )) ) ;

theorem :: FLANG_2:53
for x, E being ( ( ) ( ) set )
for A being ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) )
for m, n being ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) holds
( <%x : ( ( ) ( ) set ) %> : ( ( V15() V20() ) ( non empty V8() V15() V18( NAT : ( ( ) ( non empty V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) V20() V33() V40(1 : ( ( ) ( non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V51() ) set ) in A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) |^ (m : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) ,n : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) ) : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) iff ( <%x : ( ( ) ( ) set ) %> : ( ( V15() V20() ) ( non empty V8() V15() V18( NAT : ( ( ) ( non empty V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) V20() V33() V40(1 : ( ( ) ( non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V51() ) set ) in A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) & m : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) <= n : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) & ( ( <%> E : ( ( ) ( ) set ) : ( ( ) ( empty V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative V15() V16() V17() V18( NAT : ( ( ) ( non empty V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) V19(b2 : ( ( ) ( ) set ) ) V20() V21() V22() V23() V32() V33() V34() V37() V51() ) Element of K231(b2 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b2 : ( ( ) ( ) set ) )) ) in A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) & n : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) > 0 : ( ( ) ( empty V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative V15() V16() V17() V18( NAT : ( ( ) ( non empty V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) V20() V21() V22() V23() V32() V33() V34() V37() V51() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) or ( m : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) <= 1 : ( ( ) ( non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) & 1 : ( ( ) ( non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) <= n : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) ) ) ) ) ;

theorem :: FLANG_2:54
for E being ( ( ) ( ) set )
for A, B being ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) )
for m, n being ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) holds (A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) /\ B : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( V23() ) Element of K6((b1 : ( ( ) ( ) set ) ^omega) : ( ( ) ( non empty V23() ) set ) ) : ( ( ) ( non empty ) set ) ) |^ (m : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) ,n : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) ) : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) c= (A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) |^ (m : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) ,n : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) )) : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) /\ (B : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) |^ (m : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) ,n : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) )) : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( V23() ) Element of K6((b1 : ( ( ) ( ) set ) ^omega) : ( ( ) ( non empty V23() ) set ) ) : ( ( ) ( non empty ) set ) ) ;

theorem :: FLANG_2:55
for E being ( ( ) ( ) set )
for A, B being ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) )
for m, n being ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) holds (A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) |^ (m : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) ,n : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) )) : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) \/ (B : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) |^ (m : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) ,n : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) )) : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( V23() ) Element of K6((b1 : ( ( ) ( ) set ) ^omega) : ( ( ) ( non empty V23() ) set ) ) : ( ( ) ( non empty ) set ) ) c= (A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) \/ B : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( V23() ) Element of K6((b1 : ( ( ) ( ) set ) ^omega) : ( ( ) ( non empty V23() ) set ) ) : ( ( ) ( non empty ) set ) ) |^ (m : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) ,n : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) ) : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) ;

theorem :: FLANG_2:56
for E being ( ( ) ( ) set )
for A being ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) )
for m, n, k, l being ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) holds (A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) |^ (m : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) ,n : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) )) : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) |^ (k : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) ,l : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) ) : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) c= A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) |^ ((m : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) * k : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) ) : ( ( ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) set ) ,(n : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) * l : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) ) : ( ( ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) set ) ) : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) ;

theorem :: FLANG_2:57
for E being ( ( ) ( ) set )
for B, A being ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) )
for m, n being ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) st m : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) <= n : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) & <%> E : ( ( ) ( ) set ) : ( ( ) ( empty V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative V15() V16() V17() V18( NAT : ( ( ) ( non empty V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) V19(b1 : ( ( ) ( ) set ) ) V20() V21() V22() V23() V32() V33() V34() V37() V51() ) Element of K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) in B : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) holds
( A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) c= A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) ^^ (B : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) |^ (m : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) ,n : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) )) : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( V23() ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) & A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) c= (B : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) |^ (m : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) ,n : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) )) : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) ^^ A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( V23() ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) ) ;

theorem :: FLANG_2:58
for E being ( ( ) ( ) set )
for A, C, B being ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) )
for m, n, k, l being ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) st m : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) <= n : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) & k : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) <= l : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) & A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) c= C : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) |^ (m : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) ,n : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) ) : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) & B : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) c= C : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) |^ (k : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) ,l : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) ) : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) holds
A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) ^^ B : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( V23() ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) c= C : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) |^ ((m : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) + k : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) ) : ( ( ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) set ) ,(n : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) + l : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) ) : ( ( ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) set ) ) : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) ;

theorem :: FLANG_2:59
for E being ( ( ) ( ) set )
for A being ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) )
for m, n being ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) holds (A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) |^ (m : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) ,n : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) )) : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) * : ( ( ) ( V23() ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) c= A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) * : ( ( ) ( V23() ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) ;

theorem :: FLANG_2:60
for E being ( ( ) ( ) set )
for A being ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) )
for m, n being ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) holds (A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) *) : ( ( ) ( V23() ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) |^ (m : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) ,n : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) ) : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) c= A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) * : ( ( ) ( V23() ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) ;

theorem :: FLANG_2:61
for E being ( ( ) ( ) set )
for A being ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) )
for m, n being ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) st m : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) <= n : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) & n : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) > 0 : ( ( ) ( empty V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative V15() V16() V17() V18( NAT : ( ( ) ( non empty V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) V20() V21() V22() V23() V32() V33() V34() V37() V51() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) holds
(A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) *) : ( ( ) ( V23() ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) |^ (m : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) ,n : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) ) : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) = A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) * : ( ( ) ( V23() ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) ;

theorem :: FLANG_2:62
for E being ( ( ) ( ) set )
for A being ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) )
for m, n being ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) st m : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) <= n : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) & n : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) > 0 : ( ( ) ( empty V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative V15() V16() V17() V18( NAT : ( ( ) ( non empty V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) V20() V21() V22() V23() V32() V33() V34() V37() V51() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) & <%> E : ( ( ) ( ) set ) : ( ( ) ( empty V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative V15() V16() V17() V18( NAT : ( ( ) ( non empty V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) V19(b1 : ( ( ) ( ) set ) ) V20() V21() V22() V23() V32() V33() V34() V37() V51() ) Element of K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) in A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) holds
(A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) |^ (m : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) ,n : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) )) : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) * : ( ( ) ( V23() ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) = A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) * : ( ( ) ( V23() ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) ;

theorem :: FLANG_2:63
for E being ( ( ) ( ) set )
for A being ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) )
for m, n being ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) st m : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) <= n : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) & <%> E : ( ( ) ( ) set ) : ( ( ) ( empty V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative V15() V16() V17() V18( NAT : ( ( ) ( non empty V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) V19(b1 : ( ( ) ( ) set ) ) V20() V21() V22() V23() V32() V33() V34() V37() V51() ) Element of K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) in A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) holds
(A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) |^ (m : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) ,n : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) )) : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) * : ( ( ) ( V23() ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) = (A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) *) : ( ( ) ( V23() ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) |^ (m : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) ,n : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) ) : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) ;

theorem :: FLANG_2:64
for E being ( ( ) ( ) set )
for A, B being ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) )
for m, n being ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) st A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) c= B : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) * : ( ( ) ( V23() ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) holds
A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) |^ (m : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) ,n : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) ) : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) c= B : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) * : ( ( ) ( V23() ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) ;

theorem :: FLANG_2:65
for E being ( ( ) ( ) set )
for A, B being ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) )
for m, n being ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) st A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) c= B : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) * : ( ( ) ( V23() ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) holds
B : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) * : ( ( ) ( V23() ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) = (B : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) \/ (A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) |^ (m : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) ,n : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) )) : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( V23() ) Element of K6((b1 : ( ( ) ( ) set ) ^omega) : ( ( ) ( non empty V23() ) set ) ) : ( ( ) ( non empty ) set ) ) * : ( ( ) ( V23() ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) ;

theorem :: FLANG_2:66
for E being ( ( ) ( ) set )
for A being ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) )
for m, n being ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) holds (A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) |^ (m : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) ,n : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) )) : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) ^^ (A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) *) : ( ( ) ( V23() ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( V23() ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) = (A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) *) : ( ( ) ( V23() ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) ^^ (A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) |^ (m : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) ,n : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) )) : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( V23() ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) ;

theorem :: FLANG_2:67
for E being ( ( ) ( ) set )
for A being ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) )
for m, n being ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) st <%> E : ( ( ) ( ) set ) : ( ( ) ( empty V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative V15() V16() V17() V18( NAT : ( ( ) ( non empty V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) V19(b1 : ( ( ) ( ) set ) ) V20() V21() V22() V23() V32() V33() V34() V37() V51() ) Element of K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) in A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) & m : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) <= n : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) holds
A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) * : ( ( ) ( V23() ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) = (A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) *) : ( ( ) ( V23() ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) ^^ (A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) |^ (m : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) ,n : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) )) : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( V23() ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) ;

theorem :: FLANG_2:68
for E being ( ( ) ( ) set )
for A being ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) )
for m, n, k being ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) holds (A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) |^ (m : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) ,n : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) )) : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) |^ k : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) : ( ( ) ( V23() ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) c= A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) * : ( ( ) ( V23() ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) ;

theorem :: FLANG_2:69
for E being ( ( ) ( ) set )
for A being ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) )
for k, m, n being ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) holds (A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) |^ k : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) ) : ( ( ) ( V23() ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) |^ (m : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) ,n : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) ) : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) c= A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) * : ( ( ) ( V23() ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) ;

theorem :: FLANG_2:70
for E being ( ( ) ( ) set )
for A being ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) )
for m, n being ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) st m : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) <= n : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) holds
(A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) |^ m : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) ) : ( ( ) ( V23() ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) * : ( ( ) ( V23() ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) c= (A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) |^ (m : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) ,n : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) )) : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) * : ( ( ) ( V23() ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) ;

theorem :: FLANG_2:71
for E being ( ( ) ( ) set )
for A being ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) )
for m, n, k, l being ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) holds (A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) |^ (m : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) ,n : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) )) : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) |^ (k : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) ,l : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) ) : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) c= A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) * : ( ( ) ( V23() ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) ;

theorem :: FLANG_2:72
for E being ( ( ) ( ) set )
for A being ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) )
for k, n, l being ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) st <%> E : ( ( ) ( ) set ) : ( ( ) ( empty V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative V15() V16() V17() V18( NAT : ( ( ) ( non empty V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) V19(b1 : ( ( ) ( ) set ) ) V20() V21() V22() V23() V32() V33() V34() V37() V51() ) Element of K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) in A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) & k : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) <= n : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) & l : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) <= n : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) holds
A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) |^ (k : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) ,n : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) ) : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) = A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) |^ (l : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) ,n : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) ) : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) ;

begin

definition
let E be ( ( ) ( ) set ) ;
let A be ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) ;
func A ? -> ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) equals :: FLANG_2:def 2
 union { B : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) where B is ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) : ex k being ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) st
( k : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) <= 1 : ( ( ) ( non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) & B : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) = A : ( ( ) ( V23() ) Element of K6(K231(E : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(E : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) |^ k : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) : ( ( ) ( V23() ) Element of K6(K231(E : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(E : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) ) } : ( ( ) ( ) set ) ;
end;

theorem :: FLANG_2:73
for E, x being ( ( ) ( ) set )
for A being ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) holds
( x : ( ( ) ( ) set ) in A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) ? : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) iff ex k being ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) st
( k : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) <= 1 : ( ( ) ( non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) & x : ( ( ) ( ) set ) in A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) |^ k : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) : ( ( ) ( V23() ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) ) ) ;

theorem :: FLANG_2:74
for E being ( ( ) ( ) set )
for A being ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) )
for n being ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) st n : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) <= 1 : ( ( ) ( non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) holds
A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) |^ n : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) : ( ( ) ( V23() ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) c= A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) ? : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) ;

theorem :: FLANG_2:75
for E being ( ( ) ( ) set )
for A being ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) holds A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) ? : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) = (A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) |^ 0 : ( ( ) ( empty V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative V15() V16() V17() V18( NAT : ( ( ) ( non empty V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) V20() V21() V22() V23() V32() V33() V34() V37() V51() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( V23() ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) \/ (A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) |^ 1 : ( ( ) ( non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( V23() ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( V23() ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) ;

theorem :: FLANG_2:76
for E being ( ( ) ( ) set )
for A being ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) holds A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) ? : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) = {(<%> E : ( ( ) ( ) set ) ) : ( ( ) ( empty V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative V15() V16() V17() V18( NAT : ( ( ) ( non empty V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) V19(b1 : ( ( ) ( ) set ) ) V20() V21() V22() V23() V32() V33() V34() V37() V51() ) Element of K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) } : ( ( ) ( non empty V23() V33() V37() ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) \/ A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty V23() ) Element of K6((b1 : ( ( ) ( ) set ) ^omega) : ( ( ) ( non empty V23() ) set ) ) : ( ( ) ( non empty ) set ) ) ;

theorem :: FLANG_2:77
for E being ( ( ) ( ) set )
for A being ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) holds A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) c= A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) ? : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) ;

theorem :: FLANG_2:78
for x, E being ( ( ) ( ) set )
for A being ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) holds
( x : ( ( ) ( ) set ) in A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) ? : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) iff ( x : ( ( ) ( ) set ) = <%> E : ( ( ) ( ) set ) : ( ( ) ( empty V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative V15() V16() V17() V18( NAT : ( ( ) ( non empty V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) V19(b2 : ( ( ) ( ) set ) ) V20() V21() V22() V23() V32() V33() V34() V37() V51() ) Element of K231(b2 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b2 : ( ( ) ( ) set ) )) ) or x : ( ( ) ( ) set ) in A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) ) ) ;

theorem :: FLANG_2:79
for E being ( ( ) ( ) set )
for A being ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) holds A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) ? : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) = A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) |^ (0 : ( ( ) ( empty V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative V15() V16() V17() V18( NAT : ( ( ) ( non empty V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) V20() V21() V22() V23() V32() V33() V34() V37() V51() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) ;

theorem :: FLANG_2:80
for E being ( ( ) ( ) set )
for A being ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) holds
( A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) ? : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) = A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) iff <%> E : ( ( ) ( ) set ) : ( ( ) ( empty V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative V15() V16() V17() V18( NAT : ( ( ) ( non empty V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) V19(b1 : ( ( ) ( ) set ) ) V20() V21() V22() V23() V32() V33() V34() V37() V51() ) Element of K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) in A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) ) ;

registration
let E be ( ( ) ( ) set ) ;
let A be ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) ;
cluster A : ( ( ) ( V23() ) Element of K6((E : ( ( ) ( ) set ) ^omega) : ( ( ) ( non empty V23() ) set ) ) : ( ( ) ( non empty ) set ) ) ? : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) -> non empty ;
end;

theorem :: FLANG_2:81
for E being ( ( ) ( ) set )
for A being ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) holds (A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) ?) : ( ( ) ( non empty V23() ) Subset of ( ( ) ( non empty ) set ) ) ? : ( ( ) ( non empty V23() ) Subset of ( ( ) ( non empty ) set ) ) = A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) ? : ( ( ) ( non empty V23() ) Subset of ( ( ) ( non empty ) set ) ) ;

theorem :: FLANG_2:82
for E being ( ( ) ( ) set )
for A, B being ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) st A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) c= B : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) holds
A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) ? : ( ( ) ( non empty V23() ) Subset of ( ( ) ( non empty ) set ) ) c= B : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) ? : ( ( ) ( non empty V23() ) Subset of ( ( ) ( non empty ) set ) ) ;

theorem :: FLANG_2:83
for x, E being ( ( ) ( ) set )
for A being ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) st x : ( ( ) ( ) set ) in A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) & x : ( ( ) ( ) set ) <> <%> E : ( ( ) ( ) set ) : ( ( ) ( empty V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative V15() V16() V17() V18( NAT : ( ( ) ( non empty V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) V19(b2 : ( ( ) ( ) set ) ) V20() V21() V22() V23() V32() V33() V34() V37() V51() ) Element of K231(b2 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b2 : ( ( ) ( ) set ) )) ) holds
A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) ? : ( ( ) ( non empty V23() ) Subset of ( ( ) ( non empty ) set ) ) <> {(<%> E : ( ( ) ( ) set ) ) : ( ( ) ( empty V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative V15() V16() V17() V18( NAT : ( ( ) ( non empty V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) V19(b2 : ( ( ) ( ) set ) ) V20() V21() V22() V23() V32() V33() V34() V37() V51() ) Element of K231(b2 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b2 : ( ( ) ( ) set ) )) ) } : ( ( ) ( non empty V23() V33() V37() ) Element of K6(K231(b2 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b2 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) ;

theorem :: FLANG_2:84
for E being ( ( ) ( ) set )
for A being ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) holds
( A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) ? : ( ( ) ( non empty V23() ) Subset of ( ( ) ( non empty ) set ) ) = {(<%> E : ( ( ) ( ) set ) ) : ( ( ) ( empty V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative V15() V16() V17() V18( NAT : ( ( ) ( non empty V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) V19(b1 : ( ( ) ( ) set ) ) V20() V21() V22() V23() V32() V33() V34() V37() V51() ) Element of K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) } : ( ( ) ( non empty V23() V33() V37() ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) iff ( A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) = {} : ( ( ) ( empty V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative V15() V16() V17() V18( NAT : ( ( ) ( non empty V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) V20() V21() V22() V23() V32() V33() V34() V37() V51() ) set ) or A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) = {(<%> E : ( ( ) ( ) set ) ) : ( ( ) ( empty V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative V15() V16() V17() V18( NAT : ( ( ) ( non empty V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) V19(b1 : ( ( ) ( ) set ) ) V20() V21() V22() V23() V32() V33() V34() V37() V51() ) Element of K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) } : ( ( ) ( non empty V23() V33() V37() ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) ) ) ;

theorem :: FLANG_2:85
for E being ( ( ) ( ) set )
for A being ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) holds
( (A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) *) : ( ( ) ( V23() ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) ? : ( ( ) ( non empty V23() ) Subset of ( ( ) ( non empty ) set ) ) = A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) * : ( ( ) ( V23() ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) & (A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) ?) : ( ( ) ( non empty V23() ) Subset of ( ( ) ( non empty ) set ) ) * : ( ( ) ( V23() ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) = A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) * : ( ( ) ( V23() ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) ) ;

theorem :: FLANG_2:86
for E being ( ( ) ( ) set )
for A being ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) holds A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) ? : ( ( ) ( non empty V23() ) Subset of ( ( ) ( non empty ) set ) ) c= A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) * : ( ( ) ( V23() ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) ;

theorem :: FLANG_2:87
for E being ( ( ) ( ) set )
for A, B being ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) holds (A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) /\ B : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( V23() ) Element of K6((b1 : ( ( ) ( ) set ) ^omega) : ( ( ) ( non empty V23() ) set ) ) : ( ( ) ( non empty ) set ) ) ? : ( ( ) ( non empty V23() ) Subset of ( ( ) ( non empty ) set ) ) = (A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) ?) : ( ( ) ( non empty V23() ) Subset of ( ( ) ( non empty ) set ) ) /\ (B : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) ?) : ( ( ) ( non empty V23() ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( V23() ) Element of K6((b1 : ( ( ) ( ) set ) ^omega) : ( ( ) ( non empty V23() ) set ) ) : ( ( ) ( non empty ) set ) ) ;

theorem :: FLANG_2:88
for E being ( ( ) ( ) set )
for A, B being ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) holds (A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) ?) : ( ( ) ( non empty V23() ) Subset of ( ( ) ( non empty ) set ) ) \/ (B : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) ?) : ( ( ) ( non empty V23() ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty V23() ) Element of K6((b1 : ( ( ) ( ) set ) ^omega) : ( ( ) ( non empty V23() ) set ) ) : ( ( ) ( non empty ) set ) ) = (A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) \/ B : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( V23() ) Element of K6((b1 : ( ( ) ( ) set ) ^omega) : ( ( ) ( non empty V23() ) set ) ) : ( ( ) ( non empty ) set ) ) ? : ( ( ) ( non empty V23() ) Subset of ( ( ) ( non empty ) set ) ) ;

theorem :: FLANG_2:89
for x, E being ( ( ) ( ) set )
for A being ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) st A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) ? : ( ( ) ( non empty V23() ) Subset of ( ( ) ( non empty ) set ) ) = {x : ( ( ) ( ) set ) } : ( ( ) ( non empty V33() ) set ) holds
x : ( ( ) ( ) set ) = <%> E : ( ( ) ( ) set ) : ( ( ) ( empty V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative V15() V16() V17() V18( NAT : ( ( ) ( non empty V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) V19(b2 : ( ( ) ( ) set ) ) V20() V21() V22() V23() V32() V33() V34() V37() V51() ) Element of K231(b2 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b2 : ( ( ) ( ) set ) )) ) ;

theorem :: FLANG_2:90
for E, x being ( ( ) ( ) set )
for A being ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) holds
( <%x : ( ( ) ( ) set ) %> : ( ( V15() V20() ) ( non empty V8() V15() V18( NAT : ( ( ) ( non empty V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) V20() V33() V40(1 : ( ( ) ( non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V51() ) set ) in A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) ? : ( ( ) ( non empty V23() ) Subset of ( ( ) ( non empty ) set ) ) iff <%x : ( ( ) ( ) set ) %> : ( ( V15() V20() ) ( non empty V8() V15() V18( NAT : ( ( ) ( non empty V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) V20() V33() V40(1 : ( ( ) ( non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) V51() ) set ) in A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) ) ;

theorem :: FLANG_2:91
for E being ( ( ) ( ) set )
for A being ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) holds (A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) ?) : ( ( ) ( non empty V23() ) Subset of ( ( ) ( non empty ) set ) ) ^^ A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( V23() ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) = A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) ^^ (A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) ?) : ( ( ) ( non empty V23() ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( V23() ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) ;

theorem :: FLANG_2:92
for E being ( ( ) ( ) set )
for A being ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) holds (A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) ?) : ( ( ) ( non empty V23() ) Subset of ( ( ) ( non empty ) set ) ) ^^ A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( V23() ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) = A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) |^ (1 : ( ( ) ( non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) ,2 : ( ( ) ( non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) ;

theorem :: FLANG_2:93
for E being ( ( ) ( ) set )
for A being ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) holds (A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) ?) : ( ( ) ( non empty V23() ) Subset of ( ( ) ( non empty ) set ) ) ^^ (A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) ?) : ( ( ) ( non empty V23() ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( V23() ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) = A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) |^ (0 : ( ( ) ( empty V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative V15() V16() V17() V18( NAT : ( ( ) ( non empty V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) V20() V21() V22() V23() V32() V33() V34() V37() V51() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) ,2 : ( ( ) ( non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) ;

theorem :: FLANG_2:94
for E being ( ( ) ( ) set )
for A being ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) )
for k being ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) holds (A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) ?) : ( ( ) ( non empty V23() ) Subset of ( ( ) ( non empty ) set ) ) |^ k : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) : ( ( ) ( V23() ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) = (A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) ?) : ( ( ) ( non empty V23() ) Subset of ( ( ) ( non empty ) set ) ) |^ (0 : ( ( ) ( empty V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative V15() V16() V17() V18( NAT : ( ( ) ( non empty V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) V20() V21() V22() V23() V32() V33() V34() V37() V51() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) ,k : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) ) : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) ;

theorem :: FLANG_2:95
for E being ( ( ) ( ) set )
for A being ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) )
for k being ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) holds (A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) ?) : ( ( ) ( non empty V23() ) Subset of ( ( ) ( non empty ) set ) ) |^ k : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) : ( ( ) ( V23() ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) = A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) |^ (0 : ( ( ) ( empty V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative V15() V16() V17() V18( NAT : ( ( ) ( non empty V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) V20() V21() V22() V23() V32() V33() V34() V37() V51() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) ,k : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) ) : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) ;

theorem :: FLANG_2:96
for E being ( ( ) ( ) set )
for A being ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) )
for m, n being ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) st m : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) <= n : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) holds
(A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) ?) : ( ( ) ( non empty V23() ) Subset of ( ( ) ( non empty ) set ) ) |^ (m : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) ,n : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) ) : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) = (A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) ?) : ( ( ) ( non empty V23() ) Subset of ( ( ) ( non empty ) set ) ) |^ (0 : ( ( ) ( empty V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative V15() V16() V17() V18( NAT : ( ( ) ( non empty V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) V20() V21() V22() V23() V32() V33() V34() V37() V51() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) ,n : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) ) : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) ;

theorem :: FLANG_2:97
for E being ( ( ) ( ) set )
for A being ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) )
for n being ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) holds (A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) ?) : ( ( ) ( non empty V23() ) Subset of ( ( ) ( non empty ) set ) ) |^ (0 : ( ( ) ( empty V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative V15() V16() V17() V18( NAT : ( ( ) ( non empty V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) V20() V21() V22() V23() V32() V33() V34() V37() V51() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) ,n : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) ) : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) = A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) |^ (0 : ( ( ) ( empty V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative V15() V16() V17() V18( NAT : ( ( ) ( non empty V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) V20() V21() V22() V23() V32() V33() V34() V37() V51() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) ,n : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) ) : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) ;

theorem :: FLANG_2:98
for E being ( ( ) ( ) set )
for A being ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) )
for m, n being ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) st m : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) <= n : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) holds
(A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) ?) : ( ( ) ( non empty V23() ) Subset of ( ( ) ( non empty ) set ) ) |^ (m : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) ,n : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) ) : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) = A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) |^ (0 : ( ( ) ( empty V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative V15() V16() V17() V18( NAT : ( ( ) ( non empty V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) V20() V21() V22() V23() V32() V33() V34() V37() V51() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) ,n : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) ) : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) ;

theorem :: FLANG_2:99
for E being ( ( ) ( ) set )
for A being ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) )
for n being ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) holds (A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) |^ (1 : ( ( ) ( non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) ,n : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) )) : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) ? : ( ( ) ( non empty V23() ) Subset of ( ( ) ( non empty ) set ) ) = A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) |^ (0 : ( ( ) ( empty V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative V15() V16() V17() V18( NAT : ( ( ) ( non empty V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) V20() V21() V22() V23() V32() V33() V34() V37() V51() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) ,n : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) ) : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) ;

theorem :: FLANG_2:100
for E being ( ( ) ( ) set )
for A, B being ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) st <%> E : ( ( ) ( ) set ) : ( ( ) ( empty V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative V15() V16() V17() V18( NAT : ( ( ) ( non empty V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) V19(b1 : ( ( ) ( ) set ) ) V20() V21() V22() V23() V32() V33() V34() V37() V51() ) Element of K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) in A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) & <%> E : ( ( ) ( ) set ) : ( ( ) ( empty V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative V15() V16() V17() V18( NAT : ( ( ) ( non empty V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) V19(b1 : ( ( ) ( ) set ) ) V20() V21() V22() V23() V32() V33() V34() V37() V51() ) Element of K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) in B : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) holds
( A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) ? : ( ( ) ( non empty V23() ) Subset of ( ( ) ( non empty ) set ) ) c= A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) ^^ B : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( V23() ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) & A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) ? : ( ( ) ( non empty V23() ) Subset of ( ( ) ( non empty ) set ) ) c= B : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) ^^ A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( V23() ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) ) ;

theorem :: FLANG_2:101
for E being ( ( ) ( ) set )
for A, B being ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) holds
( A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) c= A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) ^^ (B : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) ?) : ( ( ) ( non empty V23() ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( V23() ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) & A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) c= (B : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) ?) : ( ( ) ( non empty V23() ) Subset of ( ( ) ( non empty ) set ) ) ^^ A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( V23() ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) ) ;

theorem :: FLANG_2:102
for E being ( ( ) ( ) set )
for A, C, B being ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) st A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) c= C : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) ? : ( ( ) ( non empty V23() ) Subset of ( ( ) ( non empty ) set ) ) & B : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) c= C : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) ? : ( ( ) ( non empty V23() ) Subset of ( ( ) ( non empty ) set ) ) holds
A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) ^^ B : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( V23() ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) c= C : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) |^ (0 : ( ( ) ( empty V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative V15() V16() V17() V18( NAT : ( ( ) ( non empty V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) V20() V21() V22() V23() V32() V33() V34() V37() V51() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) ,2 : ( ( ) ( non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) ;

theorem :: FLANG_2:103
for E being ( ( ) ( ) set )
for A being ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) )
for n being ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) st <%> E : ( ( ) ( ) set ) : ( ( ) ( empty V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative V15() V16() V17() V18( NAT : ( ( ) ( non empty V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) V19(b1 : ( ( ) ( ) set ) ) V20() V21() V22() V23() V32() V33() V34() V37() V51() ) Element of K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) in A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) & n : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) > 0 : ( ( ) ( empty V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative V15() V16() V17() V18( NAT : ( ( ) ( non empty V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) V20() V21() V22() V23() V32() V33() V34() V37() V51() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) holds
A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) ? : ( ( ) ( non empty V23() ) Subset of ( ( ) ( non empty ) set ) ) c= A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) |^ n : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) : ( ( ) ( V23() ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) ;

theorem :: FLANG_2:104
for E being ( ( ) ( ) set )
for A being ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) )
for k being ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) holds (A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) ?) : ( ( ) ( non empty V23() ) Subset of ( ( ) ( non empty ) set ) ) ^^ (A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) |^ k : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) ) : ( ( ) ( V23() ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( V23() ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) = (A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) |^ k : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) ) : ( ( ) ( V23() ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) ^^ (A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) ?) : ( ( ) ( non empty V23() ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( V23() ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) ;

theorem :: FLANG_2:105
for E being ( ( ) ( ) set )
for A, B being ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) st A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) c= B : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) * : ( ( ) ( V23() ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) holds
A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) ? : ( ( ) ( non empty V23() ) Subset of ( ( ) ( non empty ) set ) ) c= B : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) * : ( ( ) ( V23() ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) ;

theorem :: FLANG_2:106
for E being ( ( ) ( ) set )
for A, B being ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) st A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) c= B : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) * : ( ( ) ( V23() ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) holds
B : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) * : ( ( ) ( V23() ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) = (B : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) \/ (A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) ?) : ( ( ) ( non empty V23() ) Subset of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty V23() ) Element of K6((b1 : ( ( ) ( ) set ) ^omega) : ( ( ) ( non empty V23() ) set ) ) : ( ( ) ( non empty ) set ) ) * : ( ( ) ( V23() ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) ;

theorem :: FLANG_2:107
for E being ( ( ) ( ) set )
for A being ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) holds (A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) ?) : ( ( ) ( non empty V23() ) Subset of ( ( ) ( non empty ) set ) ) ^^ (A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) *) : ( ( ) ( V23() ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( V23() ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) = (A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) *) : ( ( ) ( V23() ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) ^^ (A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) ?) : ( ( ) ( non empty V23() ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( V23() ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) ;

theorem :: FLANG_2:108
for E being ( ( ) ( ) set )
for A being ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) holds (A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) ?) : ( ( ) ( non empty V23() ) Subset of ( ( ) ( non empty ) set ) ) ^^ (A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) *) : ( ( ) ( V23() ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( V23() ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) = A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) * : ( ( ) ( V23() ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) ;

theorem :: FLANG_2:109
for E being ( ( ) ( ) set )
for A being ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) )
for k being ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) holds (A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) ?) : ( ( ) ( non empty V23() ) Subset of ( ( ) ( non empty ) set ) ) |^ k : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) : ( ( ) ( V23() ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) c= A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) * : ( ( ) ( V23() ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) ;

theorem :: FLANG_2:110
for E being ( ( ) ( ) set )
for A being ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) )
for k being ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) holds (A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) |^ k : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) ) : ( ( ) ( V23() ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) ? : ( ( ) ( non empty V23() ) Subset of ( ( ) ( non empty ) set ) ) c= A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) * : ( ( ) ( V23() ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) ;

theorem :: FLANG_2:111
for E being ( ( ) ( ) set )
for A being ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) )
for m, n being ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) holds (A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) ?) : ( ( ) ( non empty V23() ) Subset of ( ( ) ( non empty ) set ) ) ^^ (A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) |^ (m : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) ,n : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) )) : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( V23() ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) = (A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) |^ (m : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) ,n : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) )) : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) ^^ (A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) ?) : ( ( ) ( non empty V23() ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( V23() ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) ;

theorem :: FLANG_2:112
for E being ( ( ) ( ) set )
for A being ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) )
for k being ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) holds (A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) ?) : ( ( ) ( non empty V23() ) Subset of ( ( ) ( non empty ) set ) ) ^^ (A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) |^ k : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) ) : ( ( ) ( V23() ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( V23() ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) = A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) |^ (k : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) ,(k : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) + 1 : ( ( ) ( non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() ) set ) ) : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) ;

theorem :: FLANG_2:113
for E being ( ( ) ( ) set )
for A being ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) )
for m, n being ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) holds (A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) ?) : ( ( ) ( non empty V23() ) Subset of ( ( ) ( non empty ) set ) ) |^ (m : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) ,n : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) ) : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) c= A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) * : ( ( ) ( V23() ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) ;

theorem :: FLANG_2:114
for E being ( ( ) ( ) set )
for A being ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) )
for m, n being ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) holds (A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) |^ (m : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) ,n : ( ( V10() ) ( V4() V5() V6() V10() V11() ext-real non negative V32() ) Nat) )) : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) ? : ( ( ) ( non empty V23() ) Subset of ( ( ) ( non empty ) set ) ) c= A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) * : ( ( ) ( V23() ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) ;

theorem :: FLANG_2:115
for E being ( ( ) ( ) set )
for A being ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) holds A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) ? : ( ( ) ( non empty V23() ) Subset of ( ( ) ( non empty ) set ) ) = (A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) \ {(<%> E : ( ( ) ( ) set ) ) : ( ( ) ( empty V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative V15() V16() V17() V18( NAT : ( ( ) ( non empty V4() V5() V6() ) Element of K6(REAL : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) V19(b1 : ( ( ) ( ) set ) ) V20() V21() V22() V23() V32() V33() V34() V37() V51() ) Element of K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) } : ( ( ) ( non empty V23() V33() V37() ) Element of K6(K231(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty V23() ) M9(b1 : ( ( ) ( ) set ) )) ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( V23() ) Element of K6((b1 : ( ( ) ( ) set ) ^omega) : ( ( ) ( non empty V23() ) set ) ) : ( ( ) ( non empty ) set ) ) ? : ( ( ) ( non empty V23() ) Subset of ( ( ) ( non empty ) set ) ) ;

theorem :: FLANG_2:116
for E being ( ( ) ( ) set )
for A, B being ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) st A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) c= B : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) ? : ( ( ) ( non empty V23() ) Subset of ( ( ) ( non empty ) set ) ) holds
A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) ? : ( ( ) ( non empty V23() ) Subset of ( ( ) ( non empty ) set ) ) c= B : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) ? : ( ( ) ( non empty V23() ) Subset of ( ( ) ( non empty ) set ) ) ;

theorem :: FLANG_2:117
for E being ( ( ) ( ) set )
for A, B being ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) st A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) c= B : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) ? : ( ( ) ( non empty V23() ) Subset of ( ( ) ( non empty ) set ) ) holds
B : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) ? : ( ( ) ( non empty V23() ) Subset of ( ( ) ( non empty ) set ) ) = (B : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) \/ A : ( ( ) ( V23() ) Subset of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( V23() ) Element of K6((b1 : ( ( ) ( ) set ) ^omega) : ( ( ) ( non empty V23() ) set ) ) : ( ( ) ( non empty ) set ) ) ? : ( ( ) ( non empty V23() ) Subset of ( ( ) ( non empty ) set ) ) ;