let FT be non empty filled RelStr ; :: thesis: for A being Subset of FT holds A c= A ^b

let A be Subset of FT; :: thesis: A c= A ^b

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in A or x in A ^b )

assume A1: x in A ; :: thesis: x in A ^b

then reconsider y = x as Element of FT ;

y in U_FT y by Def4;

then U_FT y meets A by A1, XBOOLE_0:3;

hence x in A ^b ; :: thesis: verum

let A be Subset of FT; :: thesis: A c= A ^b

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in A or x in A ^b )

assume A1: x in A ; :: thesis: x in A ^b

then reconsider y = x as Element of FT ;

y in U_FT y by Def4;

then U_FT y meets A by A1, XBOOLE_0:3;

hence x in A ^b ; :: thesis: verum