meet
F
c=
D
proof
A1
:
meet
F
c=
union
F
by
Th2
;
let
x
be
object
;
:: according to
TARSKI:def 3
:: thesis:
( not
x
in
meet
F
or
x
in
D
)
assume
x
in
meet
F
;
:: thesis:
x
in
D
then
x
in
union
F
by
A1
;
hence
x
in
D
;
:: thesis:
verum
end;
hence
meet
F
is
Subset
of
D
;
:: thesis:
verum