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

proof

let u be object ; :: according to TARSKI:def 3 :: thesis: ( not u in (A ^b) /\ ([#] X9) or u in A1 ^b )
assume A3: u in (A ^b) /\ ([#] X9) ; :: thesis: u in A1 ^b
then u in A ^b by XBOOLE_0:def 4;
then consider y2 being Element of FT such that
A4: u = y2 and
A5: U_FT y2 meets A ;
reconsider y3 = y2 as Element of X9 by A3, A4;
consider z being object such that
A6: z in U_FT y2 and
A7: z in A by A5, XBOOLE_0:3;
U_FT y3 = (U_FT y2) /\ ([#] X9) 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) /\ ([#] X9)

proof

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

end;

hence A1 ^b = (A ^b) /\ ([#] X9) by A2; :: thesis: verum