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

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

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

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

then reconsider y = x as Element of FT ;

A2: y in U_FT y by Def4;

U_FT y c= A by A1, Th7;

hence x in A by A2; :: thesis: verum

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

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

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

then reconsider y = x as Element of FT ;

A2: y in U_FT y by Def4;

U_FT y c= A by A1, Th7;

hence x in A by A2; :: thesis: verum