let R be non empty void RelStr ; :: thesis: for X being Subset of R holds LAp X = [#] R
let X be Subset of R; :: thesis: LAp X = [#] R
A1: the InternalRel of R = {} by YELLOW_3:def 3;
{ x where x is Element of R : Class ({},x) c= X } = { x where x is Element of R : {} c= X }
proof
thus { x where x is Element of R : Class ({},x) c= X } c= { x where x is Element of R : {} c= X } :: according to XBOOLE_0:def 10 :: thesis: { x where x is Element of R : {} c= X } c= { x where x is Element of R : Class ({},x) c= X }
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in { x where x is Element of R : Class ({},x) c= X } or y in { x where x is Element of R : {} c= X } )
assume y in { x where x is Element of R : Class ({},x) c= X } ; :: thesis: y in { x where x is Element of R : {} c= X }
then consider z being Element of R such that
A2: ( z = y & Class ({},z) c= X ) ;
thus y in { x where x is Element of R : {} c= X } by A2; :: thesis: verum
end;
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in { x where x is Element of R : {} c= X } or y in { x where x is Element of R : Class ({},x) c= X } )
assume y in { x where x is Element of R : {} c= X } ; :: thesis: y in { x where x is Element of R : Class ({},x) c= X }
then consider z being Element of R such that
A3: ( z = y & {} c= X ) ;
Class ({},z) c= X ;
hence y in { x where x is Element of R : Class ({},x) c= X } by A3; :: thesis: verum
end;
hence LAp X = [#] R by Th2, A1; :: thesis: verum