let R be non empty RelStr ; for X, Y being Subset of R holds LAp (X /\ Y) = (LAp X) /\ (LAp Y)
let X, Y be Subset of R; LAp (X /\ Y) = (LAp X) /\ (LAp Y)
{ x where x is Element of R : Class ( the InternalRel of R,x) c= X /\ Y } = { x where x is Element of R : Class ( the InternalRel of R,x) c= X } /\ { x where x is Element of R : Class ( the InternalRel of R,x) c= Y }
proof
thus
{ x where x is Element of R : Class ( the InternalRel of R,x) c= X /\ Y } c= { x where x is Element of R : Class ( the InternalRel of R,x) c= X } /\ { x where x is Element of R : Class ( the InternalRel of R,x) c= Y }
XBOOLE_0:def 10 { x where x is Element of R : Class ( the InternalRel of R,x) c= X } /\ { x where x is Element of R : Class ( the InternalRel of R,x) c= Y } c= { x where x is Element of R : Class ( the InternalRel of R,x) c= X /\ Y } proof
let y be
object ;
TARSKI:def 3 ( not y in { x where x is Element of R : Class ( the InternalRel of R,x) c= X /\ Y } or y in { x where x is Element of R : Class ( the InternalRel of R,x) c= X } /\ { x where x is Element of R : Class ( the InternalRel of R,x) c= Y } )
assume
y in { x where x is Element of R : Class ( the InternalRel of R,x) c= X /\ Y }
;
y in { x where x is Element of R : Class ( the InternalRel of R,x) c= X } /\ { x where x is Element of R : Class ( the InternalRel of R,x) c= Y }
then consider z being
Element of
R such that A1:
(
z = y &
Class ( the
InternalRel of
R,
z)
c= X /\ Y )
;
(
X /\ Y c= X &
X /\ Y c= Y )
by XBOOLE_1:17;
then
(
Class ( the
InternalRel of
R,
z)
c= X &
Class ( the
InternalRel of
R,
z)
c= Y )
by A1;
then
(
z in { x where x is Element of R : Class ( the InternalRel of R,x) c= X } &
z in { x where x is Element of R : Class ( the InternalRel of R,x) c= Y } )
;
hence
y in { x where x is Element of R : Class ( the InternalRel of R,x) c= X } /\ { x where x is Element of R : Class ( the InternalRel of R,x) c= Y }
by A1, XBOOLE_0:def 4;
verum
end;
let y be
object ;
TARSKI:def 3 ( not y in { x where x is Element of R : Class ( the InternalRel of R,x) c= X } /\ { x where x is Element of R : Class ( the InternalRel of R,x) c= Y } or y in { x where x is Element of R : Class ( the InternalRel of R,x) c= X /\ Y } )
assume A2:
y in { x where x is Element of R : Class ( the InternalRel of R,x) c= X } /\ { x where x is Element of R : Class ( the InternalRel of R,x) c= Y }
;
y in { x where x is Element of R : Class ( the InternalRel of R,x) c= X /\ Y }
then A3:
y in { x where x is Element of R : Class ( the InternalRel of R,x) c= X }
by XBOOLE_0:def 4;
A4:
y in { x where x is Element of R : Class ( the InternalRel of R,x) c= Y }
by XBOOLE_0:def 4, A2;
consider z being
Element of
R such that A5:
(
z = y &
Class ( the
InternalRel of
R,
z)
c= X )
by A3;
consider w being
Element of
R such that A6:
(
w = y &
Class ( the
InternalRel of
R,
w)
c= Y )
by A4;
(Class ( the InternalRel of R,z)) /\ (Class ( the InternalRel of R,z)) c= X /\ Y
by A5, XBOOLE_1:27, A6;
hence
y in { x where x is Element of R : Class ( the InternalRel of R,x) c= X /\ Y }
by A5;
verum
end;
hence
LAp (X /\ Y) = (LAp X) /\ (LAp Y)
; verum