let R be non empty reflexive RelStr ; :: thesis: for X being Subset of R holds LAp X c= X

let X be Subset of R; :: thesis: LAp X c= X

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in LAp X or y in X )

assume y in LAp X ; :: thesis: y in X

then consider z being Element of R such that

A1: ( z = y & Class ( the InternalRel of R,z) c= X ) ;

A2: z in field the InternalRel of R by Th1;

A3: z in {z} by TARSKI:def 1;

[z,z] in the InternalRel of R by A2, RELAT_2:def 1, RELAT_2:def 9;

then z in the InternalRel of R .: {z} by RELAT_1:def 13, A3;

hence y in X by A1; :: thesis: verum

let X be Subset of R; :: thesis: LAp X c= X

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in LAp X or y in X )

assume y in LAp X ; :: thesis: y in X

then consider z being Element of R such that

A1: ( z = y & Class ( the InternalRel of R,z) c= X ) ;

A2: z in field the InternalRel of R by Th1;

A3: z in {z} by TARSKI:def 1;

[z,z] in the InternalRel of R by A2, RELAT_2:def 1, RELAT_2:def 9;

then z in the InternalRel of R .: {z} by RELAT_1:def 13, A3;

hence y in X by A1; :: thesis: verum