let FT be non empty RelStr ; :: thesis: for X' being non empty SubSpace of FT
for A being Subset of
for A1 being Subset of st A = A1 holds
A1 ^b = (A ^b ) /\ ([#] X')
let X' be non empty SubSpace of FT; :: thesis: for A being Subset of
for A1 being Subset of st A = A1 holds
A1 ^b = (A ^b ) /\ ([#] X')
let A be Subset of ; :: thesis: for A1 being Subset of st A = A1 holds
A1 ^b = (A ^b ) /\ ([#] X')
let A1 be Subset of ; :: thesis: ( A = A1 implies A1 ^b = (A ^b ) /\ ([#] X') )
assume A1: A = A1 ; :: thesis: A1 ^b = (A ^b ) /\ ([#] X')
A2: (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 A3: u in (A ^b ) /\ ([#] X') ; :: thesis: u in A1 ^b
then u in A ^b by XBOOLE_0:def 4;
then consider y2 being Element of such that
A4: u = y2 and
A5: U_FT y2 meets A ;
reconsider y3 = y2 as Element of by A3, A4;
consider z being set such that
A6: z in U_FT y2 and
A7: z in A by A5, XBOOLE_0:3;
U_FT y3 = (U_FT y2) /\ ([#] X') by Def2;
then z in U_FT y3 by A1, A6, A7, XBOOLE_0:def 4;
then U_FT y3 meets A1 by A1, A7, XBOOLE_0:3;
hence u in A1 ^b by A4; :: thesis: verum

end;

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

proof

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

end;

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