let Al be QC-alphabet ; :: thesis: for X, Y being Subset of (CQC-WFF Al) st X c= Y holds

Cn X c= Cn Y

let X, Y be Subset of (CQC-WFF Al); :: thesis: ( X c= Y implies Cn X c= Cn Y )

assume A1: X c= Y ; :: thesis: Cn X c= Cn Y

thus Cn X c= Cn Y :: thesis: verum

Cn X c= Cn Y

let X, Y be Subset of (CQC-WFF Al); :: thesis: ( X c= Y implies Cn X c= Cn Y )

assume A1: X c= Y ; :: thesis: Cn X c= Cn Y

thus Cn X c= Cn Y :: thesis: verum

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in Cn X or a in Cn Y )

assume A2: a in Cn X ; :: thesis: a in Cn Y

then reconsider t = a as Element of CQC-WFF Al ;

for T being Subset of (CQC-WFF Al) st T is being_a_theory & Y c= T holds

t in T

end;assume A2: a in Cn X ; :: thesis: a in Cn Y

then reconsider t = a as Element of CQC-WFF Al ;

for T being Subset of (CQC-WFF Al) st T is being_a_theory & Y c= T holds

t in T

proof

hence
a in Cn Y
by Def2; :: thesis: verum
let T be Subset of (CQC-WFF Al); :: thesis: ( T is being_a_theory & Y c= T implies t in T )

assume that

A3: T is being_a_theory and

A4: Y c= T ; :: thesis: t in T

X c= T by A1, A4;

hence t in T by A2, A3, Def2; :: thesis: verum

end;assume that

A3: T is being_a_theory and

A4: Y c= T ; :: thesis: t in T

X c= T by A1, A4;

hence t in T by A2, A3, Def2; :: thesis: verum