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