let C be FormalContext; [(phi C),(psi C)] is co-Galois
A1:
LattPOSet (BooleLatt the carrier' of C) = RelStr(# the carrier of (BooleLatt the carrier' of C),(LattRel (BooleLatt the carrier' of C)) #)
by LATTICE3:def 2;
A2:
LattPOSet (BooleLatt the carrier of C) = RelStr(# the carrier of (BooleLatt the carrier of C),(LattRel (BooleLatt the carrier of C)) #)
by LATTICE3:def 2;
A3:
for x being Element of
for y being Element of st y <= (phi C) . x holds
x <= (psi C) . y
proof
let x be
Element of ;
for y being Element of st y <= (phi C) . x holds
x <= (psi C) . ylet y be
Element of ;
( y <= (phi C) . x implies x <= (psi C) . y )
assume
y <= (phi C) . x
;
x <= (psi C) . y
then
[y,((phi C) . x)] in the
InternalRel of
(BoolePoset the carrier' of C)
by ORDERS_2:def 9;
then A4:
[y,((phi C) . x)] in LattRel (BooleLatt the carrier' of C)
by A1, YELLOW_1:def 2;
reconsider x' =
(phi C) . x as
Element of
by A1, YELLOW_1:def 2;
reconsider x =
x as
Element of
by A2, YELLOW_1:def 2;
reconsider x =
x as
Subset of
by LATTICE3:def 1;
reconsider y =
y as
Element of
by A1, YELLOW_1:def 2;
y [= x'
by A4, FILTER_1:32;
then A5:
y "\/" x' = x'
by LATTICES:def 3;
reconsider x' =
x' as
Subset of
by LATTICE3:def 1;
reconsider y =
y as
Subset of
by LATTICE3:def 1;
for
z being
set st
z in y holds
z in x'
by A5, XBOOLE_0:def 3;
then
y c= x'
by TARSKI:def 3;
then A6:
(AttributeDerivation C) . x' c= (AttributeDerivation C) . y
by Th4;
reconsider y =
y as
Element of ;
reconsider y' =
(psi C) . y as
Element of
by A2, YELLOW_1:def 2;
reconsider y' =
y' as
Subset of
by LATTICE3:def 1;
reconsider y' =
y' as
Element of ;
A7:
x c= (AttributeDerivation C) . ((ObjectDerivation C) . x)
by Th5;
reconsider x =
x as
Subset of ;
reconsider x =
x as
Element of ;
x "\/" y' = y'
by A6, A7, XBOOLE_1:1, XBOOLE_1:12;
then
x [= y'
by LATTICES:def 3;
then
[x,((psi C) . y)] in LattRel (BooleLatt the carrier of C)
by FILTER_1:32;
then
[x,((psi C) . y)] in the
InternalRel of
(BoolePoset the carrier of C)
by A2, YELLOW_1:def 2;
hence
x <= (psi C) . y
by ORDERS_2:def 9;
verum
end;
for x being Element of
for y being Element of st x <= (psi C) . y holds
y <= (phi C) . x
proof
let x be
Element of ;
for y being Element of st x <= (psi C) . y holds
y <= (phi C) . xlet y be
Element of ;
( x <= (psi C) . y implies y <= (phi C) . x )
assume
x <= (psi C) . y
;
y <= (phi C) . x
then
[x,((psi C) . y)] in the
InternalRel of
(BoolePoset the carrier of C)
by ORDERS_2:def 9;
then A8:
[x,((psi C) . y)] in LattRel (BooleLatt the carrier of C)
by A2, YELLOW_1:def 2;
reconsider y' =
(psi C) . y as
Element of
by A2, YELLOW_1:def 2;
reconsider y =
y as
Element of
by A1, YELLOW_1:def 2;
reconsider y =
y as
Subset of
by LATTICE3:def 1;
reconsider x =
x as
Element of
by A2, YELLOW_1:def 2;
x [= y'
by A8, FILTER_1:32;
then A9:
x "\/" y' = y'
by LATTICES:def 3;
reconsider y' =
y' as
Subset of
by LATTICE3:def 1;
reconsider x =
x as
Subset of
by LATTICE3:def 1;
for
z being
set st
z in x holds
z in y'
by A9, XBOOLE_0:def 3;
then A10:
x c= y'
by TARSKI:def 3;
reconsider x =
x,
y' =
y' as
Subset of ;
A11:
(ObjectDerivation C) . y' c= (ObjectDerivation C) . x
by A10, Th3;
reconsider x =
x as
Element of ;
reconsider x' =
(phi C) . x as
Element of
by A1, YELLOW_1:def 2;
reconsider x' =
x' as
Subset of
by LATTICE3:def 1;
reconsider x' =
x' as
Element of ;
A12:
y c= (ObjectDerivation C) . ((AttributeDerivation C) . y)
by Th6;
reconsider y =
y as
Element of ;
y "\/" x' = x'
by A11, A12, XBOOLE_1:1, XBOOLE_1:12;
then
y [= x'
by LATTICES:def 3;
then
[y,((phi C) . x)] in LattRel (BooleLatt the carrier' of C)
by FILTER_1:32;
then
[y,((phi C) . x)] in the
InternalRel of
(BoolePoset the carrier' of C)
by A1, YELLOW_1:def 2;
hence
y <= (phi C) . x
by ORDERS_2:def 9;
verum
end;
hence
[(phi C),(psi C)] is co-Galois
by A3, Th13; verum