let FT be non empty RelStr ; :: thesis: for X' being non empty SubSpace of FT
for A being Subset of FT
for A1 being Subset of X' st A = A1 holds
A1 ^b = (A ^b ) /\ ([#] X')
let X' be non empty SubSpace of FT; :: thesis: for A being Subset of FT
for A1 being Subset of X' st A = A1 holds
A1 ^b = (A ^b ) /\ ([#] X')
let A be Subset of FT; :: thesis: for A1 being Subset of X' st A = A1 holds
A1 ^b = (A ^b ) /\ ([#] X')
let A1 be Subset of X'; :: thesis: ( A = A1 implies A1 ^b = (A ^b ) /\ ([#] X') )
assume A1: A = A1 ; :: thesis: A1 ^b = (A ^b ) /\ ([#] X')
A2: A1 ^b c= (A ^b ) /\ ([#] X')

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in A1 ^b or x in (A ^b ) /\ ([#] X') )
assume A3: x in A1 ^b ; :: thesis: x in (A ^b ) /\ ([#] X')
reconsider Y = X' as non empty RelStr ;
consider y being Element of Y such that
A4: ( y = x & U_FT y meets A1 ) by A3;
A5: y in the carrier of X' ;
the carrier of Y c= the carrier of FT by Def2;
then reconsider z = y as Element of FT by A5;
U_FT y = (Im the InternalRel of FT,y) /\ the carrier of X' by Def2;
then U_FT z meets A by A1, A4, XBOOLE_1:74;
then z in { u where u is Element of FT : U_FT u meets A } ;
hence x in (A ^b ) /\ ([#] X') by A4, XBOOLE_0:def 4; :: thesis: verum

end;

(A ^b ) /\ ([#] X') c= A1 ^b

proof

let u be set ; :: according to TARSKI:def 3 :: thesis: ( not u in (A ^b ) /\ ([#] X') or u in A1 ^b )
assume A6: u in (A ^b ) /\ ([#] X') ; :: thesis: u in A1 ^b
then ( u in A ^b & u in [#] X' ) by XBOOLE_0:def 4;
then consider y2 being Element of FT such that
A7: ( u = y2 & U_FT y2 meets A ) ;
reconsider y3 = y2 as Element of X' by A6, A7;
consider z being set such that
A8: ( z in U_FT y2 & z in A ) by A7, XBOOLE_0:3;
U_FT y3 = (U_FT y2) /\ ([#] X') by Def2;
then z in U_FT y3 by A1, A8, XBOOLE_0:def 4;
then U_FT y3 meets A1 by A1, A8, XBOOLE_0:3;
hence u in A1 ^b by A7; :: thesis: verum

end;

hence A1 ^b = (A ^b ) /\ ([#] X') by A2, XBOOLE_0:def 10; :: thesis: verum