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

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

A1 ^b c= (A ^b) /\ ([#] X9)
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;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

proof

hence
A1 ^b = (A ^b) /\ ([#] X9)
by A2; :: thesis: verum
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;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