let FT be non empty RelStr ; :: thesis: for A, B being Subset of FT st A c= B holds

A ^b c= B ^b

let A, B be Subset of FT; :: thesis: ( A c= B implies A ^b c= B ^b )

assume A1: A c= B ; :: thesis: A ^b c= B ^b

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

assume A2: x in A ^b ; :: thesis: x in B ^b

then reconsider y = x as Element of FT ;

U_FT y meets A by A2, Th8;

then ex w being object st

( w in U_FT y & w in A ) by XBOOLE_0:3;

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

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

A ^b c= B ^b

let A, B be Subset of FT; :: thesis: ( A c= B implies A ^b c= B ^b )

assume A1: A c= B ; :: thesis: A ^b c= B ^b

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

assume A2: x in A ^b ; :: thesis: x in B ^b

then reconsider y = x as Element of FT ;

U_FT y meets A by A2, Th8;

then ex w being object st

( w in U_FT y & w in A ) by XBOOLE_0:3;

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

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